the proof FLAT:

(DECL (FLAT) |GROUND⊗GROUND→GROUND| CONSTANT)
1. NIL
   deps: NIL

(AXIOM |∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))|)
2. ∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))
   deps: NIL

(COMMENTL LNAME DEFINFO)
3. NIL
   deps: NIL

(DECL (FLATTEN) |GROUND→GROUND| CONSTANT)
4. NIL
   deps: NIL

(AXIOM
 |∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)|)
5. ∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)
   deps: NIL

(COMMENTL LNAME DEFINFO)
6. NIL
   deps: NIL

(LINENAME LISTPFLATTEN *)


(COMMENTL LNAME LISTPFLATTEN)
7. NIL
   deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL*
  ([1#1#2](&DEFINFO**SIMPINFO*NIL))| LISTPFLATTEN SORTINFO)
8. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
          (∀U.FLAT(X,FLAT(Y,U))=FLATTEN(X)*FLATTEN(Y)*U))⊃
    (∀X U.FLAT(X,U)=FLATTEN(X)*U)
   deps: NIL

(ASSUME |(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)|)
9. (∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)
   deps: (9)